no\_repeats($T$; $l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$i$:$\mathbb{N}$, $j$:$\mathbb{N}$. ($i$ $<$ $\parallel$$l$$\parallel$) $\Rightarrow$ ($j$ $<$ $\parallel$$l$$\parallel$) $\Rightarrow$ ($\neg$($i$ = $j$ $\in$ $\mathbb{N}$)) $\Rightarrow$ ($\neg$($l$[$i$] = $l$[$j$] $\in$ $T$))